forall a: forall b:
L:a;L:a,b = L:a,b